\begin{tabbing} $\forall$\=${\it es}$:ES, $T$, $A$:Type, $l$:IdLnk, ${\it tg}$, $a$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$Prop),\+ \\[0ex]$f$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$$T$). \-\\[0ex]weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$) $\in$ Prop \end{tabbing}